es:ES, i:Id, ds:x:Id fp Type, I:(State(ds)).
@i discrete ds
 e@i. (first(e))  I((state when e))
 e@i. I((state when e))  I(state after e)
 e@i. I((state when e)) 

latex

Definitions	A c B, x. t(x), t  T, P & Q, x(s), e@i. P(e), P  Q, , a:A fp B(a), x:A. B(x), P  Q, {T}, SQType(T), P  Q
Lemmas	state-after-pred-ds, event system wf, Id wf, l member wf, decl-state wf, es-dds wf, es-state-after wf, alle-at wf, es-first wf, assert wf, not wf, es-loc wf, es-loc-pred, es-pred wf, Id sq, es-state-subtype2, es-state-when wf, alle-at-iff